Failed to solve the following constraints:
  Is empty: f true ≡ f false
      [ at Issue2250.agda:19,10-12 ]
